1. Field of the Invention
This invention relates to analyzing errors in computer programs. More specifically, the invention relates to identifying errors in computer programs and to specifying test cases that will cause the errors to occur.
2. Background Art
There are several known methods for identifying errors in software programs. The most common of these methods is testing; that is, executing the target program under different conditions in order to confirm its correct behavior. Another group of methods, program verifiers, attempt to prove mathematically that a program's behavior is correct for all possible input conditions. In addition, there are static analysis tools that perform a set of limited checks without executing the program. These tools report some possible errors.
There are numerous testing tools for exposing errors in a software program. With these tools, the user is provided with an environment for specifying program values, for executing the program in steps, and for examining the resulting program values.
A program verifier attempts to prove that a formal assertion of correct behavior is true for all possible inputs and for all possible execution paths. If the proof is successful, there are no errors represented by the assertion in this portion of the program. If the assertion is proved false, a set of conditions is identified that specify the program's erroneous behavior. Program verifiers are discussed, for instance, in “Predicate Abstraction For Software Verification,” by Cormac Flanagan and Shaz Qadeer, Proceedings of the 29th ACM SIGPLA-SIGACT symposium on Principles of programming languages, Vol. 37, Issue 1, Jan. 2002.
Another class of tools, referred to as Weak Status Analysis tools, use syntactic and data-flow analysis techniques found in compilers to identify possible program errors. These techniques do identify some program errors, but do not consider the Boolean conditions controlling a program execution and therefore also produce some false error reports.
Other static analysis tools, referred to as Strong Static Analysis tools, use additional theorem proving and symbolic execution techniques to reduce the number of false error reports and to specify the program conditions that lead to an erroneous program execution. One known Strong Static Analysis tool is the Beam analysis tool. The Beam analysis tool is discussed in “A Software Falsifier,” by Daniel Brand, International symposium on Software Reliability Engineering, pp. 174–185, October 2000.
While there is a wide range of existing tools to identify program errors, each approach has its limitations.
More specifically, while testing is the most common method for finding errors, it is known that the effectiveness of testing is limited by a user's ability to create new test cases that explore a program's different behaviors. It is normally not feasible to test all possible program executions and is extremely difficult to know what area of a program's execution to explore.
Verifiers require precise and detailed specifications of the target program's correct behavior as well as the surrounding environment of the program execution. Still, it is often the case that an assertion about a program's correctness cannot be shown to be either true or false. This may be due to the limitations of the verifier or of the specification. User assistance is usually needed to guide and to attempt to complete the proof.
Weak Static Analysis tools usually require no additional user input or specifications, but typically produce a large number of false error reports. This is because these tools do not analyze the Boolean conditions that determine a program's control flow, and therefore usually are uncertain if the error will actually occur in the program's actual execution. The user must sort through the false errors to find the real errors reported.
The additional theorem proving and symbolic execution techniques used in Strong Static Analysis tools, such as the Beam tool, do reduce the number of false error reports. However, no method can resolve all conditions in a program and false error reports are still a possibility. For instance, when the Beam analysis tool cannot determine if a particular error will occur in actual program execution, this tool chooses not to report the potential error. This conservative policy has the effect of greatly reducing the number of false error reports, but at the expense of ignoring some potential errors.